Home > Search Results: keywords:"silně-separační logika"
Search:
Search Tips :: Advanced Search
Search collections:
Sort by: Display results: Output format:
National Repository of Grey Literature 2 records found  Search took 0.00 seconds. 
A Decision Procedure for Strong-Separation Logic
 Dacík, Tomáš ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Separační logika (SL) patří mezi nejúspěšnější nástroje pro verifikaci programů pracujících s dynamicky alokovanou pamětí. Její vysoká expresivita ovšem přináší nerozhodnutelnost pokud formule kombinují více jejích spojek, především separační implikace. Jako řešení byla navrhnuta takzvaná silně-separační logika (SSL), která díky striktnější definici sémantiky rozšiřuje rozhodnutelný fragment a přitom zůstává vhodná pro verifikaci programů. V současnosti ale neexistuje žádná implementace rozhodovací procedury pro tuto logiku. Tato práce se zaměřuje na návrh a implementaci rozhodovací procedury pro SSL založené na překladu vstupní formule na formuli v prvořádové logice, jejíž splnitelnost je poté možné ověřit pomocí specializovaných nástrojů. Experimentální výsledky na omezeném fragmentu, kde SL a SSL splývají, ukazují, že navržený nástroj je schopen efektivně řešit formule pocházející z verifikačních nástrojů a výrazně překonává všechny ostatní existující rozhodovací procedury, které jsou také založené na překladu. Během experimentů jsme také odhalili několik případů nekorektnosti heuristik použitých v rozhodovací proceduře pro SL implementované v nástroji cvc5. Na základě našich hlášení byly tyto heuristiky opraveny.
Detailed record
A Decision Procedure for Strong-Separation Logic
 Dacík, Tomáš ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Separační logika (SL) patří mezi nejúspěšnější nástroje pro verifikaci programů pracujících s dynamicky alokovanou pamětí. Její vysoká expresivita ovšem přináší nerozhodnutelnost pokud formule kombinují více jejích spojek, především separační implikace. Jako řešení byla navrhnuta takzvaná silně-separační logika (SSL), která díky striktnější definici sémantiky rozšiřuje rozhodnutelný fragment a přitom zůstává vhodná pro verifikaci programů. V současnosti ale neexistuje žádná implementace rozhodovací procedury pro tuto logiku. Tato práce se zaměřuje na návrh a implementaci rozhodovací procedury pro SSL založené na překladu vstupní formule na formuli v prvořádové logice, jejíž splnitelnost je poté možné ověřit pomocí specializovaných nástrojů. Experimentální výsledky na omezeném fragmentu, kde SL a SSL splývají, ukazují, že navržený nástroj je schopen efektivně řešit formule pocházející z verifikačních nástrojů a výrazně překonává všechny ostatní existující rozhodovací procedury, které jsou také založené na překladu. Během experimentů jsme také odhalili několik případů nekorektnosti heuristik použitých v rozhodovací proceduře pro SL implementované v nástroji cvc5. Na základě našich hlášení byly tyto heuristiky opraveny.
Detailed record

Interested in being notified about new results for this query?
Subscribe to the RSS feed.
Digital Repository :: Search :: Submit :: Personalize :: Help
Powered by Invenio v1.1.2
Maintained by admin.invenio@techlib.cz
This site is also available in the following languages:
Česky  English